The naming of the i.MX boards is inconsistent, ARM Sabre Lite is iMX.6 but i.MX8MM-EVK is referred to as iMX8 MM and IMX8MM-EVK. Is the platform field supposed to be human readable or is it supposed to be seL4's name for the platform?

The config ARM Sabre Lite says that its platform is iMX.6 (e.g. Sabre Lite). The e.g implies that the Sabre Lite is one kind of platform that is supported, but the title implies only the Sabre Lite is supported? What is correct?

Another comment (not relevant to this PR) is that all the 32-bit ARM configs are named differently depending if hypervisor mode is supported or not but the AARCH64 configuration does not have HYP in the name, even though it does support hypervisor mode.

Another comment (not relevant to this PR) is that all the 32-bit ARM configs are named differently depending if hypervisor mode is supported or not but the AARCH64 configuration does not have HYP in the name, even though it does support hypervisor mode.

From memory this is a historical thing which probably can't be changed at this point but it's one of the things that makes this page more confusing than it should be (in my opinion).

Another comment (not relevant to this PR) is that all the 32-bit ARM configs are named differently depending if hypervisor mode is supported or not but the AARCH64 configuration does not have HYP in the name, even though it does support hypervisor mode.

From memory this is a historical thing which probably can't be changed at this point but it's one of the things that makes this page more confusing than it should be (in my opinion).

It's something we eventually want to get rid of (but currently can't for the old stuff), so we've decided to keep it clean for AARCH64 at least. It does make it inconsistent, but the hope is to resolve that in the future.

The naming of the i.MX boards is inconsistent, ARM Sabre Lite is iMX.6 but i.MX8MM-EVK is referred to as iMX8 MM and IMX8MM-EVK. Is the platform field supposed to be human readable or is it supposed to be seL4's name for the platform?

The config ARM Sabre Lite says that its platform is iMX.6 (e.g. Sabre Lite). The e.g implies that the Sabre Lite is one kind of platform that is supported, but the title implies only the Sabre Lite is supported? What is correct?

Tbh, I was confused about that as well. The config file for just ARM has set(KernelPlatform "imx6" CACHE STRING "") which does not explicitly select sabre, but sabre is then picked as default and it is relatively certain that other boards will not work automatically. So the e.g. is wrong.

I guess this means the heading for the other one should be i.MX8MM-EVK

Ok, I've pushed a new version with an attempt at more consistency. The platform/soc/board names are already not very consistent in the main hardware table, esp between the imx platforms. I've defaulted to using the same string as in that table (which gives is ARM IMX8MM-EVK for that config we talked about above), and I've removed the e.g. bits from the table that were a bit misleading.

arm_hyp could be removed, it's a big change, but doesn't affect verification and so should be tractable.

arm_hyp could be removed, it's a big change, but doesn't affect verification and so should be tractable.

We might be talking about different ARM_HYP things -- ARM_HYP is the name of the verification L4V_ARCH setting that selects the Arm 32 bit proofs with hyp. It's also a cmake setting. The cmake setting could be changed without affecting verification, I think, but the name would still be mentioned on this page because the name also encodes proof selection.

Ok, I've pushed a new version with an attempt at more consistency. The platform/soc/board names are already not very consistent in the main hardware table, esp between the imx platforms. I've defaulted to using the same string as in that table (which gives is ARM IMX8MM-EVK for that config we talked about above), and I've removed the e.g. bits from the table that were a bit misleading.

Thanks for making it less confusing!